Left Termination proof of /tmp/tmpmFGcVR/balance

Left Termination of the query pattern
balance(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 364 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 70 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 306 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇒, 6 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

(0) Obligation:

Clauses:

balance(T, TB) :- balance(T, -(I, []), -(.(','(TB, -(I, [])), X), X), -(Rest, []), -(Rest, [])).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(NH, NT)) :- ','(balance(L, -(IH, .(V, IT1)), -(H, T), -(HR1, TR1), -(NH, NT1)), balance(R, -(IT1, IT), -(HR1, TR1), -(HR, TR), -(NT1, NT))).

Query: balance(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: balance(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: balance(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, []))\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 1 | balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), balance(T27, -(X108, []), -(X109, X110), -(X116, []), -(X111, [])))\n\nT25 is ground\nT26 is ground\nT27 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111))\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, []))\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 1 | balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 1\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(balance(T142, -(T156, .(T143, X245)), -(.(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157), -(X246, X247), -(X252, X248)), balance(T144, -(X245, .(T146, X249)), -(X246, X247), -(X250, X251), -(X248, X253)))\n\nT142 is ground\nT143 is ground\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX252 is free\nX253 is free\nX245 is free\nX246 is free\nX247 is free\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: balance(T142, -(T156, .(T143, X245)), -(.(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157), -(X246, X247), -(X252, X248))\n\nT142 is ground\nT143 is ground\nX252 is free\nX245 is free\nX246 is free\nX247 is free\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253))\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 1 | balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 2\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 1\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 2\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(balance(T291, -(T305, .(T292, X380)), -(T306, T307), -(X381, X382), -(T308, X383)), balance(T293, -(X380, .(T295, X384)), -(X381, X382), -(X385, X386), -(X383, X387)))\n\nT291 is ground\nT292 is ground\nT293 is ground\nT295 is ground\nX384 is free\nX385 is free\nX386 is free\nX387 is free\nX380 is free\nX381 is free\nX382 is free\nX383 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: balance(T291, -(T305, .(T292, X380)), -(T306, T307), -(X381, X382), -(T308, X383))\n\nT291 is ground\nT292 is ground\nX380 is free\nX381 is free\nX382 is free\nX383 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: balance(T293, -(T323, .(T295, X384)), -(T324, T325), -(X385, X386), -(T326, X387))\n\nT293 is ground\nT295 is ground\nX384 is free\nX385 is free\nX386 is free\nX387 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 1 | balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 1\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(balance(T418, -(T432, .(T419, X508)), -(T433, T434), -(X509, X510), -(T435, X511)), balance(T420, -(X508, []), -(X509, X510), -(T436, []), -(X511, [])))\n\nT418 is ground\nT419 is ground\nT420 is ground\nX508 is free\nX509 is free\nX510 is free\nX511 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: balance(T418, -(T432, .(T419, X508)), -(T433, T434), -(X509, X510), -(T435, X511))\n\nT418 is ground\nT419 is ground\nX508 is free\nX509 is free\nX510 is free\nX511 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: balance(T420, -(T451, []), -(T452, T453), -(T455, []), -(T454, []))\n\nT420 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 44 [arrowhead = none ];
44 -> 2;

45 [label="ONLY EVAL with clause\nbalance(X3, X4) :- balance(X3, -(X5, []), -(.(','(X4, -(X5, [])), X6), X6), -(X7, []), -(X7, [])).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 45 [arrowhead = none ];
45 -> 3;

46 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 46 [arrowhead = none ];
46 -> 4;

47 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 47 [arrowhead = none ];
47 -> 5;

48 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 48 [arrowhead = none ];
48 -> 6;

49 [label="EVAL with clause\nbalance(nil, -(X36, X36), -(X37, X38), -(X37, X38), -(.(','(nil, -(X39, X39)), X40), X40)).\nand substitutionT5 -> nil,\nX5 -> [],\nX36 -> [],\nX41 -> [],\nT7 -> nil,\nX6 -> [],\nX37 -> .(','(nil, -([], [])), []),\nX38 -> [],\nX7 -> .(','(nil, -([], [])), []),\nX42 -> [],\nT12 -> nil,\nX39 -> [],\nX40 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 49 [arrowhead = none ];
49 -> 7;

50 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 50 [arrowhead = none ];
50 -> 8;

51 [label="EVAL with clause\nbalance(tree(X91, X92, X93), -(X94, X95), -(.(','(tree(X96, X97, X98), -(X99, X100)), X101), .(','(X96, -(X99, .(X97, X102))), .(','(X98, -(X102, X100)), X103))), -(X104, X105), -(X106, X107)) :- ','(balance(X91, -(X94, .(X92, X108)), -(X101, X103), -(X109, X110), -(X106, X111)), balance(X93, -(X108, X95), -(X109, X110), -(X104, X105), -(X111, X107))).\nand substitutionX91 -> T25,\nX92 -> T26,\nX93 -> T27,\nT5 -> tree(T25, T26, T27),\nX5 -> T31,\nX94 -> T31,\nX95 -> [],\nX96 -> T33,\nX97 -> T34,\nX98 -> T36,\nT7 -> tree(T33, T34, T36),\nX99 -> T31,\nX100 -> [],\nX6 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX101 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX102 -> T35,\nX103 -> T32,\nX113 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX7 -> X116,\nX104 -> X116,\nX105 -> [],\nX106 -> X116,\nX107 -> [],\nX112 -> T31,\nX115 -> T32,\nT28 -> T33,\nT29 -> T34,\nX114 -> T35,\nT30 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 51 [arrowhead = none ];
51 -> 10;

52 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 52 [arrowhead = none ];
52 -> 11;

53 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 53 [arrowhead = none ];
53 -> 9;

54 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
10 -> 54 [arrowhead = none ];
54 -> 12;

55 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nreplacements:X108 -> T53,\nX109 -> T54,\nX110 -> T55,\nX116 -> T56,\nX111 -> T57", fontsize=14, style = filled, fillcolor = violet];
10 -> 55 [arrowhead = none ];
55 -> 13;

56 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 56 [arrowhead = none ];
56 -> 14;

57 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 57 [arrowhead = none ];
57 -> 34;

58 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 58 [arrowhead = none ];
58 -> 15;

59 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 59 [arrowhead = none ];
59 -> 16;

60 [label="EVAL with clause\nbalance(nil, -(X173, X173), -(X174, X175), -(X174, X175), -(.(','(nil, -(X176, X176)), X177), X177)).\nand substitutionT25 -> nil,\nT31 -> .(T107, T108),\nX173 -> .(T107, T108),\nT26 -> T107,\nX108 -> T108,\nT106 -> .(T107, T108),\nT33 -> T109,\nT34 -> T110,\nT35 -> T111,\nT36 -> T112,\nT32 -> T113,\nX174 -> .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)),\nX175 -> T113,\nX109 -> .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)),\nX110 -> T113,\nX176 -> X178,\nX177 -> X179,\nX116 -> .(','(nil, -(X178, X178)), X179),\nX111 -> X179", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 60 [arrowhead = none ];
60 -> 17;

61 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 61 [arrowhead = none ];
61 -> 18;

62 [label="EVAL with clause\nbalance(tree(X228, X229, X230), -(X231, X232), -(.(','(tree(X233, X234, X235), -(X236, X237)), X238), .(','(X233, -(X236, .(X234, X239))), .(','(X235, -(X239, X237)), X240))), -(X241, X242), -(X243, X244)) :- ','(balance(X228, -(X231, .(X229, X245)), -(X238, X240), -(X246, X247), -(X243, X248)), balance(X230, -(X245, X232), -(X246, X247), -(X241, X242), -(X248, X244))).\nand substitutionX228 -> T142,\nX229 -> T143,\nX230 -> T144,\nT25 -> tree(T142, T143, T144),\nT31 -> T156,\nX231 -> T156,\nT26 -> T146,\nX108 -> X249,\nX232 -> .(T146, X249),\nX233 -> T160,\nX234 -> T161,\nX235 -> T163,\nT33 -> tree(T160, T161, T163),\nX236 -> T156,\nT34 -> T164,\nT35 -> T159,\nX237 -> .(T164, T159),\nT36 -> T158,\nT32 -> .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)),\nX238 -> .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))),\nX239 -> T162,\nX240 -> T157,\nT153 -> .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)),\nX109 -> X250,\nX241 -> X250,\nX110 -> X251,\nX242 -> X251,\nX116 -> X252,\nX243 -> X252,\nX111 -> X253,\nX244 -> X253,\nT145 -> T156,\nT155 -> T157,\nT152 -> T158,\nT151 -> T159,\nT147 -> T160,\nT148 -> T161,\nT154 -> T162,\nT149 -> T163,\nT150 -> T164", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 62 [arrowhead = none ];
62 -> 20;

63 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 63 [arrowhead = none ];
63 -> 21;

64 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 64 [arrowhead = none ];
64 -> 19;

65 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 65 [arrowhead = none ];
65 -> 22;

66 [label="SPLIT 2\nnew knowledge:\nT142 is ground\nreplacements:X245 -> T187,\nX246 -> T188,\nX247 -> T189,\nX252 -> T190,\nX248 -> T191", fontsize=14, style = filled, fillcolor = violet];
20 -> 66 [arrowhead = none ];
66 -> 23;

67 [label="INSTANCE with matching:\nT144 -> T142\nT187 -> T156\nT146 -> T143\nX249 -> X245\nT188 -> .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)))\nT189 -> T157\nX250 -> X246\nX251 -> X247\nT191 -> X252\nX253 -> X248", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 67 [arrowhead = none , style=dashed];
67 -> 23[style=dashed];

68 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 68 [arrowhead = none ];
68 -> 24;

69 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 69 [arrowhead = none ];
69 -> 25;

70 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 70 [arrowhead = none ];
70 -> 26;

71 [label="EVAL with clause\nbalance(nil, -(X312, X312), -(X313, X314), -(X313, X314), -(.(','(nil, -(X315, X315)), X316), X316)).\nand substitutionT144 -> nil,\nT187 -> .(T257, T258),\nX312 -> .(T257, T258),\nT146 -> T257,\nX249 -> T258,\nT256 -> .(T257, T258),\nT188 -> T259,\nX313 -> T259,\nT189 -> T260,\nX314 -> T260,\nX250 -> T259,\nX251 -> T260,\nX315 -> T261,\nX316 -> T262,\nT191 -> .(','(nil, -(T261, T261)), T262),\nX253 -> T262", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 71 [arrowhead = none ];
71 -> 27;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 72 [arrowhead = none ];
72 -> 28;

73 [label="EVAL with clause\nbalance(tree(X363, X364, X365), -(X366, X367), -(.(','(tree(X368, X369, X370), -(X371, X372)), X373), .(','(X368, -(X371, .(X369, X374))), .(','(X370, -(X374, X372)), X375))), -(X376, X377), -(X378, X379)) :- ','(balance(X363, -(X366, .(X364, X380)), -(X373, X375), -(X381, X382), -(X378, X383)), balance(X365, -(X380, X367), -(X381, X382), -(X376, X377), -(X383, X379))).\nand substitutionX363 -> T291,\nX364 -> T292,\nX365 -> T293,\nT144 -> tree(T291, T292, T293),\nT187 -> T305,\nX366 -> T305,\nT146 -> T295,\nX249 -> X384,\nX367 -> .(T295, X384),\nX368 -> T296,\nX369 -> T297,\nX370 -> T298,\nX371 -> T299,\nX372 -> T300,\nX373 -> T306,\nT188 -> .(','(tree(T296, T297, T298), -(T299, T300)), T306),\nX374 -> T302,\nX375 -> T307,\nT189 -> .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)),\nX250 -> X385,\nX376 -> X385,\nX251 -> X386,\nX377 -> X386,\nT191 -> T308,\nX378 -> T308,\nX253 -> X387,\nX379 -> X387,\nT294 -> T305,\nT301 -> T306,\nT303 -> T307,\nT304 -> T308", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 73 [arrowhead = none ];
73 -> 30;

74 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 74 [arrowhead = none ];
74 -> 31;

75 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 75 [arrowhead = none ];
75 -> 29;

76 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
30 -> 76 [arrowhead = none ];
76 -> 32;

77 [label="SPLIT 2\nnew knowledge:\nT291 is ground\nreplacements:X380 -> T323,\nX381 -> T324,\nX382 -> T325,\nX383 -> T326", fontsize=14, style = filled, fillcolor = violet];
30 -> 77 [arrowhead = none ];
77 -> 33;

78 [label="INSTANCE with matching:\nT144 -> T291\nT187 -> T305\nT146 -> T292\nX249 -> X380\nT188 -> T306\nT189 -> T307\nX250 -> X381\nX251 -> X382\nT191 -> T308\nX253 -> X383", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 78 [arrowhead = none , style=dashed];
78 -> 23[style=dashed];

79 [label="INSTANCE with matching:\nT144 -> T293\nT187 -> T323\nT146 -> T295\nX249 -> X384\nT188 -> T324\nT189 -> T325\nX250 -> X385\nX251 -> X386\nT191 -> T326\nX253 -> X387", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 79 [arrowhead = none , style=dashed];
79 -> 23[style=dashed];

80 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 80 [arrowhead = none ];
80 -> 35;

81 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 81 [arrowhead = none ];
81 -> 36;

82 [label="EVAL with clause\nbalance(nil, -(X448, X448), -(X449, X450), -(X449, X450), -(.(','(nil, -(X451, X451)), X452), X452)).\nand substitutionT27 -> nil,\nT53 -> [],\nX448 -> [],\nT385 -> [],\nT54 -> T386,\nX449 -> T386,\nT55 -> [],\nX450 -> [],\nT56 -> T386,\nT387 -> [],\nX451 -> T388,\nX452 -> [],\nT57 -> .(','(nil, -(T388, T388)), []),\nT389 -> []", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 82 [arrowhead = none ];
82 -> 37;

83 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 83 [arrowhead = none ];
83 -> 38;

84 [label="EVAL with clause\nbalance(tree(X491, X492, X493), -(X494, X495), -(.(','(tree(X496, X497, X498), -(X499, X500)), X501), .(','(X496, -(X499, .(X497, X502))), .(','(X498, -(X502, X500)), X503))), -(X504, X505), -(X506, X507)) :- ','(balance(X491, -(X494, .(X492, X508)), -(X501, X503), -(X509, X510), -(X506, X511)), balance(X493, -(X508, X495), -(X509, X510), -(X504, X505), -(X511, X507))).\nand substitutionX491 -> T418,\nX492 -> T419,\nX493 -> T420,\nT27 -> tree(T418, T419, T420),\nT53 -> T432,\nX494 -> T432,\nX495 -> [],\nX496 -> T422,\nX497 -> T423,\nX498 -> T424,\nX499 -> T425,\nX500 -> T426,\nX501 -> T433,\nT54 -> .(','(tree(T422, T423, T424), -(T425, T426)), T433),\nX502 -> T428,\nX503 -> T434,\nT55 -> .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)),\nT56 -> T436,\nX504 -> T436,\nX505 -> [],\nT57 -> T435,\nX506 -> T435,\nX507 -> [],\nT421 -> T432,\nT427 -> T433,\nT429 -> T434,\nT431 -> T435,\nT430 -> T436", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 84 [arrowhead = none ];
84 -> 40;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 85 [arrowhead = none ];
85 -> 41;

86 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 86 [arrowhead = none ];
86 -> 39;

87 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 87 [arrowhead = none ];
87 -> 42;

88 [label="SPLIT 2\nnew knowledge:\nT418 is ground\nreplacements:X508 -> T451,\nX509 -> T452,\nX510 -> T453,\nX511 -> T454,\nT436 -> T455", fontsize=14, style = filled, fillcolor = violet];
40 -> 88 [arrowhead = none ];
88 -> 43;

89 [label="INSTANCE with matching:\nT144 -> T418\nT187 -> T432\nT146 -> T419\nX249 -> X508\nT188 -> T433\nT189 -> T434\nX250 -> X509\nX251 -> X510\nT191 -> T435\nX253 -> X511", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 89 [arrowhead = none , style=dashed];
89 -> 23[style=dashed];

90 [label="INSTANCE with matching:\nT27 -> T420\nT53 -> T451\nT54 -> T452\nT55 -> T453\nT56 -> T455\nT57 -> T454", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 90 [arrowhead = none , style=dashed];
90 -> 13[style=dashed];

}

(2) Obligation:

Clauses:

balanceA(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262).
balanceA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) :- balanceA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383).
balanceA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) :- ','(balanceA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326), balanceA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)).
balanceB(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])).
balanceB(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) :- balanceA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511).
balanceB(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) :- ','(balanceA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454), balanceB(T420, T451, T452, T453, T455, T454)).
balanceC(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179).
balanceC(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) :- balanceA(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248).
balanceC(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) :- ','(balanceA(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191), balanceA(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)).
balanceD(nil, nil).
balanceD(tree(T25, T26, T27), tree(T33, T34, T36)) :- balanceC(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111).
balanceD(tree(T25, T26, T27), tree(T33, T34, T36)) :- ','(balanceC(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57), balanceB(T27, T53, T54, T55, T56, T57)).

Query: balanceD(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
balanceD_in: (b,f)
balanceC_in: (b,f,b,f,f,f,f,f,f,f,f,f,f)
balanceA_in: (b,f,b,f,f,f,f,f,f,f)
balanceB_in: (b,f,f,f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

balanceD_in_ga(nil, nil) → balanceD_out_ga(nil, nil)
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
balanceC_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceC_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253)
U10_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceB_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceB_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balanceB_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

balanceD_in_ga(nil, nil) → balanceD_out_ga(nil, nil)
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
balanceC_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceC_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253)
U10_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceB_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceB_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balanceB_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

BALANCED_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_GA(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
BALANCED_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → BALANCEC_IN_GAGAAAAAAAAAA(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)
BALANCEC_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
BALANCEC_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → BALANCEA_IN_GAGAAAAAAA(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → BALANCEA_IN_GAGAAAAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEA_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
BALANCEC_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCEA_IN_GAGAAAAAAA(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)
BALANCED_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_GA(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_GA(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCEB_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → BALANCEA_IN_GAGAAAAAAA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)
BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEB_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balanceD_in_ga(nil, nil) → balanceD_out_ga(nil, nil)
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
balanceC_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceC_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253)
U10_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceB_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceB_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balanceB_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

The argument filtering Pi contains the following mapping:
balanceD_in_ga(x1, x2) = balanceD_in_ga(x1)
nil = nil
balanceD_out_ga(x1, x2) = balanceD_out_ga
tree(x1, x2, x3) = tree(x1, x2, x3)
U10_ga(x1, x2, x3, x4, x5, x6, x7) = U10_ga(x7)
balanceC_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balanceC_in_gagaaaaaaaaaa(x1, x3)
balanceC_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balanceC_out_gagaaaaaaaaaa
U7_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_gagaaaaaaaaaa(x19)
balanceA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceA_in_gagaaaaaaa(x1, x3)
balanceA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceA_out_gagaaaaaaa
U1_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_gagaaaaaaa(x19)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x3, x5, x19)
U3_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_gagaaaaaaa(x19)
U8_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_gagaaaaaaaaaa(x3, x5, x19)
U9_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_gagaaaaaaaaaa(x19)
U11_ga(x1, x2, x3, x4, x5, x6, x7) = U11_ga(x3, x7)
U12_ga(x1, x2, x3, x4, x5, x6, x7) = U12_ga(x7)
balanceB_in_gaaaaa(x1, x2, x3, x4, x5, x6) = balanceB_in_gaaaaa(x1)
balanceB_out_gaaaaa(x1, x2, x3, x4, x5, x6) = balanceB_out_gaaaaa
U4_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_gaaaaa(x15)
U5_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_gaaaaa(x3, x15)
U6_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_gaaaaa(x15)
BALANCED_IN_GA(x1, x2) = BALANCED_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5, x6, x7) = U10_GA(x7)
BALANCEC_IN_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = BALANCEC_IN_GAGAAAAAAAAAA(x1, x3)
U7_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_GAGAAAAAAAAAA(x19)
BALANCEA_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCEA_IN_GAGAAAAAAA(x1, x3)
U1_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_GAGAAAAAAA(x19)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_GAGAAAAAAA(x3, x5, x19)
U3_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_GAGAAAAAAA(x19)
U8_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_GAGAAAAAAAAAA(x3, x5, x19)
U9_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_GAGAAAAAAAAAA(x19)
U11_GA(x1, x2, x3, x4, x5, x6, x7) = U11_GA(x3, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7) = U12_GA(x7)
BALANCEB_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = BALANCEB_IN_GAAAAA(x1)
U4_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_GAAAAA(x15)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_GAAAAA(x3, x15)
U6_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_GAAAAA(x15)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCED_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_GA(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
BALANCED_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → BALANCEC_IN_GAGAAAAAAAAAA(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)
BALANCEC_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
BALANCEC_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → BALANCEA_IN_GAGAAAAAAA(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → BALANCEA_IN_GAGAAAAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEA_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
BALANCEC_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCEA_IN_GAGAAAAAAA(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)
BALANCED_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_GA(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_GA(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCEB_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → BALANCEA_IN_GAGAAAAAAA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)
BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEB_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balanceD_in_ga(nil, nil) → balanceD_out_ga(nil, nil)
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
balanceC_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceC_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253)
U10_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceB_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceB_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balanceB_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 15 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEA_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → BALANCEA_IN_GAGAAAAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)

The TRS R consists of the following rules:

balanceD_in_ga(nil, nil) → balanceD_out_ga(nil, nil)
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
balanceC_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceC_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253)
U10_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceB_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceB_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balanceB_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEA_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → BALANCEA_IN_GAGAAAAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)

The TRS R consists of the following rules:

balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balanceA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceA_in_gagaaaaaaa(x1, x3)
balanceA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceA_out_gagaaaaaaa
U1_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_gagaaaaaaa(x19)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x3, x5, x19)
U3_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_gagaaaaaaa(x19)
BALANCEA_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCEA_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_GAGAAAAAAA(x3, x5, x19)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → U2_GAGAAAAAAA(T293, T295, balanceA_in_gagaaaaaaa(T291, T292))
U2_GAGAAAAAAA(T293, T295, balanceA_out_gagaaaaaaa) → BALANCEA_IN_GAGAAAAAAA(T293, T295)
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → BALANCEA_IN_GAGAAAAAAA(T291, T292)

The TRS R consists of the following rules:

balanceA_in_gagaaaaaaa(nil, T257) → balanceA_out_gagaaaaaaa
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U1_gagaaaaaaa(balanceA_in_gagaaaaaaa(T291, T292))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U2_gagaaaaaaa(T293, T295, balanceA_in_gagaaaaaaa(T291, T292))
U1_gagaaaaaaa(balanceA_out_gagaaaaaaa) → balanceA_out_gagaaaaaaa
U2_gagaaaaaaa(T293, T295, balanceA_out_gagaaaaaaa) → U3_gagaaaaaaa(balanceA_in_gagaaaaaaa(T293, T295))
U3_gagaaaaaaa(balanceA_out_gagaaaaaaa) → balanceA_out_gagaaaaaaa

The set Q consists of the following terms:

balanceA_in_gagaaaaaaa(x0, x1)
U1_gagaaaaaaa(x0)
U2_gagaaaaaaa(x0, x1, x2)
U3_gagaaaaaaa(x0)

We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U2_GAGAAAAAAA(T293, T295, balanceA_out_gagaaaaaaa) → BALANCEA_IN_GAGAAAAAAA(T293, T295)
The graph contains the following edges 1 >= 1, 2 >= 2
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → BALANCEA_IN_GAGAAAAAAA(T291, T292)
The graph contains the following edges 1 > 1, 1 > 2
BALANCEA_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → U2_GAGAAAAAAA(T293, T295, balanceA_in_gagaaaaaaa(T291, T292))
The graph contains the following edges 1 > 1, 2 >= 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEB_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balanceD_in_ga(nil, nil) → balanceD_out_ga(nil, nil)
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111))
balanceC_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceC_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248))
balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, X245, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X246, X247, X252, X248)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
balanceC_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, T190, X253, balanceA_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → balanceC_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, T190, X253)
U10_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balanceD_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balanceC_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balanceC_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balanceB_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceB_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceB_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balanceB_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceB_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balanceB_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balanceB_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balanceD_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEB_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balanceA_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEB_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balanceA_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceA_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, balanceA_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → balanceA_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balanceA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceA_in_gagaaaaaaa(x1, x3)
balanceA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceA_out_gagaaaaaaa
U1_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_gagaaaaaaa(x19)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x3, x5, x19)
U3_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_gagaaaaaaa(x19)
BALANCEB_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = BALANCEB_IN_GAAAAA(x1)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_GAAAAA(x3, x15)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCEB_IN_GAAAAA(tree(T418, T419, T420)) → U5_GAAAAA(T420, balanceA_in_gagaaaaaaa(T418, T419))
U5_GAAAAA(T420, balanceA_out_gagaaaaaaa) → BALANCEB_IN_GAAAAA(T420)

The TRS R consists of the following rules:

balanceA_in_gagaaaaaaa(nil, T257) → balanceA_out_gagaaaaaaa
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U1_gagaaaaaaa(balanceA_in_gagaaaaaaa(T291, T292))
balanceA_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U2_gagaaaaaaa(T293, T295, balanceA_in_gagaaaaaaa(T291, T292))
U1_gagaaaaaaa(balanceA_out_gagaaaaaaa) → balanceA_out_gagaaaaaaa
U2_gagaaaaaaa(T293, T295, balanceA_out_gagaaaaaaa) → U3_gagaaaaaaa(balanceA_in_gagaaaaaaa(T293, T295))
U3_gagaaaaaaa(balanceA_out_gagaaaaaaa) → balanceA_out_gagaaaaaaa

The set Q consists of the following terms:

balanceA_in_gagaaaaaaa(x0, x1)
U1_gagaaaaaaa(x0)
U2_gagaaaaaaa(x0, x1, x2)
U3_gagaaaaaaa(x0)

We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U5_GAAAAA(T420, balanceA_out_gagaaaaaaa) → BALANCEB_IN_GAAAAA(T420)
The graph contains the following edges 1 >= 1
BALANCEB_IN_GAAAAA(tree(T418, T419, T420)) → U5_GAAAAA(T420, balanceA_in_gagaaaaaaa(T418, T419))
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES